<html>
    <head>
        <title></title>
        <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
        <link rel="stylesheet" type="text/css" href="../style.css">
    </head>
    <body>
        <div class="text">
        <h2>Verifikations-Menü</h2>
        Im Menü „Verifikation“ stehen mehrere Möglichkeiten zur Auswahl, nachdem eine Datei geöffnet
wurde. Vor der Auswahl einer Funktion ist zunächst die Test-Datei auszuwählen, die
verarbeitet werden soll. Dies geschieht mittels eines Hinweisfensters.<br /><br />
Die Funktion „Nummerierte Ausgabe“ liest den Quelltext ein, wandelt ihn in ein internes
Format um und nummeriert jede Anweisung durch. Der Vorgang arbeitet mehrschichtig, es
gibt also nicht nur die Nummer (1), sondern evtl. auch eine Nummer (1.1.2), z.B. bei verschachtelten
Strukturen.<br /><br />
Die Funktionen „Trace“ und „Propagation“ werden jeweils in einem eigenen Kapitel dieses
Benutzerhandbuchs behandelt. Auf diese sei hier verwiesen.<br /><br />
Per Klick auf „Beweisbedarf“ werden die noch zu beweisenden Thesen aufgeführt. Hierbei
handelt es sich ausnahmslos um die Konsequenzenregel K. Stehen in der propagierten Fassung
zwei Zusicherungen direkt hintereinander, so greift diese. Mittels eines Doppelpfeils (=>) wird
jeweils verdeutlicht, was gelten muss. Dies ist - bei Bedarf - händisch zu zeigen und kann nicht
automatisiert durch dieses Programm erfolgen.
        </div>
    </body>
</html>
